(set-option :fp.spacer.gpdr true)
(declare-fun a (Bool Bool Int Int Int Int Int Int Int) Bool)
(assert (forall ((b Int) (bc Bool) (bd Bool) (bk Int) (be Int) (bf Int) (bm Int) (bn Int))
     (=> (= bc bd false) (= bk 0) (a bc bd bf b bm bn bk be b))))
(assert (forall ((bc Bool) (bd Bool) (bf Int) (bm Int) (bn Int) (bk Int) (b Int) (c Int)
         (d Int) (g Int) (e Int) (f Bool) (gn Int) (ge Int) (gl Int) (gd Bool))
     (=> (a bc bd bf b bm bn bk e b) (or (= f bc) (= bk 2)) (a f gd d gl c gn g ge e))))
(assert (forall ((bc Bool) (bd Bool) (bf Int) (bm Int) (bn Int) (bk Int) (be Int) (b Int))
     (=> (a bc bd bf b bm bn bk be b) (or bc bd) false)))
(check-sat-using horn)
(check-sat)